Inference at * 1 
Iof proof for Lemma not-not-assert:



1. b : 
2. (b)
  b 

latex

 by (SupposeNot) 
CollapseTHEN (Auto) 

latex

C.

Definitions	x:A. B(x), Dec(P), P  Q, left + right, t  T, A, P  Q, False
Lemmas	decidable assert